\begin{tabbing}
$\forall$\=${\it ds}$:fpf(Id; $x$.Type), ${\it da}$:fpf(Knd; $k$.Type), ${\it es}$:event\_system\{i:l\}, $i$:Id, $e_{1}$,$e_{2}$:\{\=$e$:es{-}E(${\it es}$)$\mid$ \+\+
\\[0ex]loc($e$) = $i$\} ,
\-\\[0ex]$L_{1}$,$L_{2}$:(event{-}info(${\it ds}$;${\it da}$) List).
\-\\[0ex]($\neg$($L_{1}$ = []))
\\[0ex]$\Rightarrow$ ($\neg$($L_{2}$ = []))
\\[0ex]$\Rightarrow$ ($\forall$$x$:Id. subtype\_rel(es{-}vartype(${\it es}$; $i$; $x$); fpf{-}cap(${\it ds}$; id{-}deq; $x$; top)))
\\[0ex]$\Rightarrow$ \=($\forall$$e$:es{-}E(${\it es}$). \+
\\[0ex](loc($e$) = $i$)
\\[0ex]$\Rightarrow$ subtype\_rel(es{-}valtype(${\it es}$; $e$); fpf{-}cap(${\it da}$; Kind{-}deq; es{-}kind(${\it es}$; $e$); top)))
\-\\[0ex]$\Rightarrow$ (es{-}hist\{i:l\}(${\it es}$;$e_{1}$;$e_{2}$) = append($L_{1}$; $L_{2}$) $\in$ (event{-}info(${\it ds}$;${\it da}$) List))
\\[0ex]$\Rightarrow$ $\exists$$e$$\in$($e_{1}$,$e_{2}$].(es{-}hist\{i:l\}(${\it es}$;$e_{1}$;es{-}pred(${\it es}$; $e$)) = $L_{1}$) $\wedge$ (es{-}hist\{i:l\}(${\it es}$;$e$;$e_{2}$) = $L_{2}$)
\end{tabbing}